Problem:
 0(1(2(x1))) -> 0(1(3(2(x1))))
 0(1(2(x1))) -> 0(2(1(0(x1))))
 0(1(2(x1))) -> 0(2(1(3(x1))))
 0(1(2(x1))) -> 0(2(2(1(x1))))
 0(1(2(x1))) -> 0(2(2(1(4(x1)))))
 0(1(2(x1))) -> 5(1(0(5(2(3(x1))))))
 0(2(4(x1))) -> 0(2(1(4(3(x1)))))
 0(4(2(x1))) -> 4(0(2(3(x1))))
 0(4(2(x1))) -> 4(0(5(5(2(x1)))))
 0(0(4(2(x1)))) -> 0(0(2(2(3(4(x1))))))
 0(1(2(2(x1)))) -> 0(2(1(0(2(x1)))))
 0(1(2(2(x1)))) -> 1(3(0(2(2(x1)))))
 0(1(2(4(x1)))) -> 0(1(4(2(3(x1)))))
 0(1(2(4(x1)))) -> 4(0(2(2(1(1(x1))))))
 0(1(2(4(x1)))) -> 4(0(5(5(2(1(x1))))))
 0(1(2(5(x1)))) -> 3(5(5(2(1(0(x1))))))
 0(1(4(2(x1)))) -> 0(5(2(1(4(x1)))))
 0(1(5(2(x1)))) -> 1(5(0(2(3(x1)))))
 0(1(5(2(x1)))) -> 0(2(2(1(0(5(x1))))))
 0(1(5(2(x1)))) -> 5(5(0(2(1(3(x1))))))
 0(2(4(2(x1)))) -> 0(5(4(3(2(2(x1))))))
 0(3(1(2(x1)))) -> 0(2(1(3(2(x1)))))
 0(3(1(2(x1)))) -> 1(0(2(5(3(x1)))))
 0(3(1(2(x1)))) -> 1(5(0(2(3(x1)))))
 0(3(1(2(x1)))) -> 3(0(2(2(1(x1)))))
 0(3(1(2(x1)))) -> 3(2(2(1(0(x1)))))
 0(3(1(2(x1)))) -> 0(3(2(3(1(3(x1))))))
 0(3(4(2(x1)))) -> 0(2(2(3(4(x1)))))
 5(0(1(2(x1)))) -> 1(3(2(5(0(x1)))))
 5(0(1(2(x1)))) -> 5(0(2(1(3(3(x1))))))
 0(1(1(2(5(x1))))) -> 5(0(2(5(1(1(x1))))))
 0(2(3(4(2(x1))))) -> 3(2(2(3(4(0(x1))))))
 0(3(1(2(5(x1))))) -> 2(3(1(3(0(5(x1))))))
 0(3(1(5(2(x1))))) -> 0(3(2(5(1(2(x1))))))
 0(3(4(1(4(x1))))) -> 0(5(3(1(4(4(x1))))))
 0(3(5(1(2(x1))))) -> 5(5(3(2(1(0(x1))))))
 0(4(0(4(2(x1))))) -> 4(4(0(0(2(2(x1))))))
 0(4(1(1(2(x1))))) -> 3(1(4(0(2(1(x1))))))
 0(4(1(2(2(x1))))) -> 4(1(0(2(2(3(x1))))))
 0(4(1(2(5(x1))))) -> 3(4(1(0(2(5(x1))))))
 0(4(2(1(2(x1))))) -> 4(1(3(2(0(2(x1))))))
 0(4(2(1(4(x1))))) -> 0(2(1(4(4(4(x1))))))
 0(4(2(5(2(x1))))) -> 5(4(3(2(2(0(x1))))))
 0(4(5(1(2(x1))))) -> 1(4(2(0(5(5(x1))))))
 0(4(5(1(2(x1))))) -> 4(0(2(5(1(1(x1))))))
 5(0(1(2(2(x1))))) -> 5(0(2(2(1(2(x1))))))
 5(0(2(4(2(x1))))) -> 0(2(2(5(1(4(x1))))))
 5(0(4(4(2(x1))))) -> 0(5(2(5(4(4(x1))))))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {6,5}
   transitions:
    01(45) -> 46*
    01(15) -> 16*
    01(142) -> 143*
    01(107) -> 108*
    01(37) -> 38*
    01(199) -> 200*
    01(179) -> 180*
    01(286) -> 287*
    01(156) -> 157*
    01(273) -> 274*
    01(153) -> 154*
    01(43) -> 44*
    01(33) -> 34*
    21(35) -> 36*
    21(25) -> 26*
    21(117) -> 118*
    21(289) -> 290*
    21(17) -> 18*
    21(12) -> 13*
    21(189) -> 190*
    21(119) -> 120*
    21(69) -> 70*
    21(226) -> 227*
    21(111) -> 112*
    21(198) -> 199*
    21(285) -> 286*
    21(23) -> 24*
    21(170) -> 171*
    21(155) -> 156*
    21(105) -> 106*
    11(77) -> 78*
    11(254) -> 255*
    11(169) -> 170*
    11(79) -> 80*
    11(34) -> 35*
    11(14) -> 15*
    11(71) -> 72*
    11(158) -> 159*
    11(108) -> 109*
    11(275) -> 276*
    11(68) -> 69*
    11(287) -> 288*
    41(187) -> 188*
    41(167) -> 168*
    41(127) -> 128*
    41(87) -> 88*
    41(274) -> 275*
    41(271) -> 272*
    41(251) -> 252*
    41(263) -> 264*
    41(253) -> 254*
    41(143) -> 144*
    41(133) -> 134*
    41(93) -> 94*
    41(265) -> 266*
    41(135) -> 136*
    41(125) -> 126*
    41(297) -> 298*
    41(95) -> 96*
    41(85) -> 86*
    31(237) -> 238*
    31(227) -> 228*
    31(217) -> 218*
    31(157) -> 158*
    31(59) -> 60*
    31(186) -> 187*
    31(61) -> 62*
    31(51) -> 52*
    31(243) -> 244*
    31(223) -> 224*
    31(290) -> 291*
    31(255) -> 256*
    31(53) -> 54*
    31(245) -> 246*
    31(235) -> 236*
    31(225) -> 226*
    31(13) -> 14*
    51(207) -> 208*
    51(197) -> 198*
    51(177) -> 178*
    51(209) -> 210*
    51(109) -> 110*
    51(201) -> 202*
    51(146) -> 147*
    51(106) -> 107*
    51(215) -> 216*
    51(145) -> 146*
    02(309) -> 310*
    00(2) -> 5*
    00(4) -> 5*
    00(1) -> 5*
    00(3) -> 5*
    52(308) -> 309*
    10(2) -> 1*
    10(4) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    22(307) -> 308*
    20(2) -> 2*
    20(4) -> 2*
    20(1) -> 2*
    20(3) -> 2*
    12(306) -> 307*
    30(2) -> 3*
    30(4) -> 3*
    30(1) -> 3*
    30(3) -> 3*
    42(319) -> 320*
    42(311) -> 312*
    42(305) -> 306*
    42(317) -> 318*
    40(2) -> 4*
    40(4) -> 4*
    40(1) -> 4*
    40(3) -> 4*
    50(2) -> 6*
    50(4) -> 6*
    50(1) -> 6*
    50(3) -> 6*
    1 -> 93,77,59,43,23
    2 -> 85,68,51,33,12
    3 -> 95,79,61,45,25
    4 -> 87,71,53,37,17
    13 -> 155,153,145
    15 -> 189*
    16 -> 38,46,154,289,44,251,217,5
    18 -> 13*
    24 -> 13*
    26 -> 13*
    34 -> 251*
    35 -> 225*
    36 -> 15*
    38 -> 34*
    44 -> 34*
    46 -> 34*
    52 -> 197,125,105,34
    54 -> 201,127,111,34
    60 -> 207,133,117,34
    62 -> 209,135,119,34
    69 -> 169*
    70 -> 273,177,35
    72 -> 69*
    78 -> 69*
    80 -> 69*
    86 -> 253,235,68
    88 -> 263,237,68
    94 -> 265,243,68
    96 -> 271,245,68
    105 -> 319*
    106 -> 285,167,142
    110 -> 44,251,5
    111 -> 317*
    112 -> 106*
    117 -> 305*
    118 -> 106*
    119 -> 311*
    120 -> 106*
    126 -> 34*
    128 -> 34*
    134 -> 34*
    136 -> 34*
    143 -> 215*
    144 -> 44,38,251,5
    147 -> 142*
    154 -> 289,34
    156 -> 186*
    159 -> 46,44,251,5
    168 -> 14*
    171 -> 105*
    178 -> 179,146
    180 -> 46,154,44,5
    188 -> 177*
    190 -> 223,15
    200 -> 158*
    202 -> 198*
    208 -> 198*
    210 -> 198*
    216 -> 158*
    218 -> 38,46,34,251,5
    224 -> 16,154,143,217,46,34,251,5
    228 -> 15*
    236 -> 35*
    238 -> 35*
    244 -> 35*
    246 -> 35*
    252 -> 227*
    254 -> 297*
    256 -> 177*
    264 -> 254*
    266 -> 254*
    272 -> 254*
    276 -> 217*
    288 -> 143*
    291 -> 287*
    298 -> 14*
    310 -> 16,5,217
    312 -> 306*
    318 -> 306*
    320 -> 306*
  problem:
   
  Qed